SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Transition system</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Transition system</span></span>

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">This article is about transition systems as used in <a href="Operational_semantics" title="Operational semantics">operational semantics</a>. For an <a href="Automata_theory" title="Automata theory">automata</a>-theoretic view, see <a href="Semiautomaton" title="Semiautomaton">semiautomaton</a>.</div>

<p>In <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a>, a <b>transition system</b> is a concept used in the study of <a href="Computation" title="Computation">computation</a>. It is used to describe the potential behavior of <a href="Discrete_system" title="Discrete system">discrete systems</a>. It consists of <a href="State_(computer_science)" title="State (computer science)">states</a> and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. If the label set is a <a href="Singleton_(mathematics)" title="Singleton (mathematics)">singleton</a>, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.

</p><p>Transition systems coincide mathematically with <a href="Abstract_rewriting_system" title="Abstract rewriting system">abstract rewriting systems</a> (as explained further in this article) and <a href="Directed_graph" title="Directed graph">directed graphs</a>. They differ from <a href="Finite-state_automata" class="mw-redirect" title="Finite-state automata">finite-state automata</a> in several ways:

</p>

<ul><li>The set of states is not necessarily finite, or even countable.</li>

<li>The set of transitions is not necessarily finite, or even countable.</li>

<li>No "start" state or "final" states are given.</li></ul>

<p>Transition systems can be represented as directed graphs.

</p>

<div class="mw-heading mw-heading2"><h2 id="Formal_definition">Formal definition</h2></div>

<p>Formally, a <b>transition system</b> is a pair <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (S,T)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (S,T)}</annotation>

</semantics>

</math></span><img src="./467faf91b93aed51e1dd1c656f1ae71d9c922a38.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.979ex; height:2.843ex;" alt="{\displaystyle (S,T)}" loading="lazy"></span> where <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math></span><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy"></span> is a set of states and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T}</annotation>

</semantics>

</math></span><img src="./ec7200acd984a1d3a3d7dc455e262fbe54f7f6e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.636ex; height:2.176ex;" alt="{\displaystyle T}" loading="lazy"></span>, the <i>transition relation</i>, is a subset of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\times S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\times S}</annotation>

</semantics>

</math></span><img src="./6b0f88969df0adf75522ab2d85717167d1069d28.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.839ex; height:2.176ex;" alt="{\displaystyle S\times S}" loading="lazy"></span>. We say that there is a transition from state <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math></span><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"></span> to state <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math></span><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"></span> if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,q)\in T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,q)\in T}</annotation>

</semantics>

</math></span><img src="./53970eaf58ef86ac30aa3070aac0e83f45600eb3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.559ex; height:2.843ex;" alt="{\displaystyle (p,q)\in T}" loading="lazy"></span>, and denote it <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\rightarrow q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\rightarrow q}</annotation>

</semantics>

</math></span><img src="./4e3f9e5de9aaead8d19411bb3ad0dc490a50ec69.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:5.942ex; height:2.176ex;" alt="{\displaystyle p\rightarrow q}" loading="lazy"></span>.

</p><p>A <b>labelled transition system</b> is a tuple <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (S,\Lambda ,T)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (S,\Lambda ,T)}</annotation>

</semantics>

</math></span><img src="./a7f4c43556289e35d4db9e464ba91c921b1a7281.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.626ex; height:2.843ex;" alt="{\displaystyle (S,\Lambda ,T)}" loading="lazy"></span> where <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math></span><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy"></span> is a set of states, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda }</annotation>

</semantics>

</math></span><img src="./0ac0a4a98a414e3480335f9ba652d12571ec6733.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.613ex; height:2.176ex;" alt="{\displaystyle \Lambda }" loading="lazy"></span> is a set of labels, and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T}</annotation>

</semantics>

</math></span><img src="./ec7200acd984a1d3a3d7dc455e262fbe54f7f6e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.636ex; height:2.176ex;" alt="{\displaystyle T}" loading="lazy"></span>, the <i>labelled transition relation</i>, is a subset of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\times \Lambda \times S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\times \Lambda \times S}</annotation>

</semantics>

</math></span><img src="./b33e37ce4a542e2949580c19ff9e01283fedd285.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.292ex; height:2.176ex;" alt="{\displaystyle S\times \Lambda \times S}" loading="lazy"></span>. We say that there is a transition from state <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math></span><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"></span> with label <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span> iff <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,\alpha ,q)\in T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,\alpha ,q)\in T}</annotation>

</semantics>

</math></span><img src="./13429863f8375e91ca83e76e6bf60a08e16ede33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.081ex; height:2.843ex;" alt="{\displaystyle (p,\alpha ,q)\in T}" loading="lazy"></span> and denote it

</p>

<mover>

</mpadded>

</mover>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\xrightarrow {\alpha } q\,.}</annotation>

</semantics>

</math></span><img src="./8bb28ff235f0dac956771f5a506064e7b4e6f318.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; margin-top: -0.391ex; width:6.976ex; height:3.676ex;" alt="{\displaystyle p\xrightarrow {\alpha } q\,.}" loading="lazy"></span></dd></dl></dd></dl>

<p>Labels can represent different things depending on the language of interest. Typical uses of labels include representing input expected, conditions that must be true to trigger the transition, or actions performed during the transition. Labelled transitions systems were originally introduced as <i>named</i> transition systems.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading3"><h3 id="Special_cases">Special cases</h3></div>

<ul><li>If, for any given <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math></span><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span>, there exists only a single tuple <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,\alpha ,q)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,\alpha ,q)}</annotation>

</semantics>

</math></span><img src="./b980d1b86b8eace672d0b458c8681bb2dddd53b6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.604ex; height:2.843ex;" alt="{\displaystyle (p,\alpha ,q)}" loading="lazy"></span> in <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T}</annotation>

</semantics>

</math></span><img src="./ec7200acd984a1d3a3d7dc455e262fbe54f7f6e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.636ex; height:2.176ex;" alt="{\displaystyle T}" loading="lazy"></span>, then one says that <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span> is <i>deterministic</i> (for <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

<li>If, for any given <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math></span><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span>, there exists at least one tuple <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,\alpha ,q)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,\alpha ,q)}</annotation>

</semantics>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T}</annotation>

</semantics>

</math></span><img src="./ec7200acd984a1d3a3d7dc455e262fbe54f7f6e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.636ex; height:2.176ex;" alt="{\displaystyle T}" loading="lazy"></span>, then one says that <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span> is <i>executable</i> (for <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

<div class="mw-heading mw-heading3"><h3 id="Coalgebra_formulation">Coalgebra formulation</h3></div>

<p>The formal definition can be rephrased as follows. Labelled state transition systems on <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math></span><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy"></span> with labels from <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda }</annotation>

</semantics>

</math></span><img src="./0ac0a4a98a414e3480335f9ba652d12571ec6733.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.613ex; height:2.176ex;" alt="{\displaystyle \Lambda }" loading="lazy"></span> correspond <a href="Bijection" title="Bijection">one-to-one</a> with functions <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}</annotation>

</semantics>

</math></span><img src="./2e1bd02ce534762713c93a6fe0433c90b3b05419.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.579ex; height:2.843ex;" alt="{\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}" loading="lazy"></span>, where <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {P}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {P}}}</annotation>

</semantics>

</math></span><img src="./10d6ec962de5797ba4f161c40e66dca74ae95cc6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.704ex; height:2.176ex;" alt="{\displaystyle {\mathcal {P}}}" loading="lazy"></span> is the (covariant) <a href="Power_set" title="Power set">powerset functor</a>. Under this bijection <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (S,\Lambda ,T)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (S,\Lambda ,T)}</annotation>

</semantics>

</math></span><img src="./a7f4c43556289e35d4db9e464ba91c921b1a7281.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.626ex; height:2.843ex;" alt="{\displaystyle (S,\Lambda ,T)}" loading="lazy"></span> is sent to <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}">

<msub>

</mrow>

</msub>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}</annotation>

</semantics>

</math></span><img src="./65bca35e9a0459290c1cdb7640fc45e40e3cc7bd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.924ex; height:2.843ex;" alt="{\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}" loading="lazy"></span>, defined by

</p>

<mover>

</mpadded>

</mover>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}}</annotation>

</semantics>

</math></span><img src="./3627f8b69aeff6d8bbf2545bb57ba6cce9a98eb7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; margin-top: -0.391ex; width:29.956ex; height:3.843ex;" alt="{\displaystyle p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}}" loading="lazy"></span>.</dd></dl></dd></dl>

<p>In other words, a labelled state transition system is a <a href="F-coalgebra" title="F-coalgebra">coalgebra</a> for the functor <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P(\Lambda \times {-})}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P(\Lambda \times {-})}</annotation>

</semantics>

</math></span><img src="./fb9dc2addfa2b736825f015ebcf2f3d954d485c0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.816ex; height:2.843ex;" alt="{\displaystyle P(\Lambda \times {-})}" loading="lazy"></span>.

</p>

<div class="mw-heading mw-heading2"><h2 id="Relation_between_labelled_and_unlabelled_transition_system">Relation between labelled and unlabelled transition system</h2></div>

<p>There are many relations between these concepts. Some are simple, such as observing that a labelled transition system where the set of labels consists of only one element is equivalent to an unlabelled transition system. However, not all these relations are equally trivial.

</p>

<div class="mw-heading mw-heading2"><h2 id="Comparison_with_abstract_rewriting_systems">Comparison with abstract rewriting systems</h2></div>

<p>As a mathematical object, an unlabeled transition system is identical with an (unindexed) <a href="Abstract_rewriting_system" title="Abstract rewriting system">abstract rewriting system</a>. If we consider the rewriting relation as an indexed set of relations, as some authors do, then a labeled transition system is equivalent to an abstract rewriting system with the indices being the labels. The focus of the study and the terminology are different, however. In a transition system one is interested in interpreting the labels as actions, whereas in an abstract rewriting system the focus is on how objects may be transformed (rewritten) into others.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Extensions">Extensions</h2></div>

<p>In <a href="Model_checking" title="Model checking">model checking</a>, a transition system is sometimes defined to include an additional labeling function for the states as well, resulting in a notion that encompasses that of <a href="Kripke_structure" class="mw-redirect" title="Kripke structure">Kripke structure</a>.<sup id="cite_ref-BaierKatoen2008_3-0" class="reference"><a href="#cite_note-BaierKatoen2008-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>

</p><p><a href="Action_language" title="Action language">Action languages</a> are extensions of transition systems, adding a set of <i>fluents</i> <i>F</i>, a set of values <i>V</i>, and a function that maps <i>F</i> × <i>S</i> to <i>V</i>.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>

</p>

<ul><li><a href="Binary_relation" title="Binary relation">Binary relation</a></li>

<li><a href="Ternary_relation" title="Ternary relation">Ternary relation</a></li>

<li><a href="Transition_monoid" class="mw-redirect" title="Transition monoid">Transition monoid</a></li>

<li><a href="Transformation_monoid" class="mw-redirect" title="Transformation monoid">Transformation monoid</a></li>

<li><a href="Semigroup_action" title="Semigroup action">Semigroup action</a></li>

<li><a href="Simulation_preorder" class="mw-redirect" title="Simulation preorder">Simulation preorder</a></li>

<li><a href="Bisimulation" title="Bisimulation">Bisimulation</a></li>

<li><a href="Operational_semantics" title="Operational semantics">Operational semantics</a></li>

<li><a href="Kripke_structure" class="mw-redirect" title="Kripke structure">Kripke structure</a></li>

<li><a href="Finite-state_machine" title="Finite-state machine">Finite-state machine</a></li>

<li><a href="Modal_%CE%BC-calculus" title="Modal μ-calculus">Modal μ-calculus</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text">Robert M. Keller (July 1976) "<a rel="nofollow" class="external text" href="https://dl.acm.org/citation.cfm?id=360251">Formal Verification of Parallel Programs</a>", <i>Communications of the ACM</i>, vol. <b>19</b>, nr. <i>7</i>, pp. 371–384.</span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text">Marc Bezem, J. W. Klop, Roel de Vrijer ("Terese"), <i>Term rewriting systems</i>, Cambridge University Press, 2003, <style data-mw-deduplicate="TemplateStyles:r1238218222">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-521-39115-6</bdi>. pp. 7–8.</span>

</li>

<li id="cite_note-BaierKatoen2008-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-BaierKatoen2008_3-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFChristel_BaierJoost-Pieter_Katoen2008" class="citation book cs1"><a href="Christel_Baier" title="Christel Baier">Christel Baier</a>; Joost-Pieter Katoen (2008). <i><a href="Principles_of_Model_Checking" title="Principles of Model Checking">Principles of Model Checking</a></i>. The MIT Press. p. 20. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-262-02649-9</bdi>.</cite></span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text">Micheal Gelfond, Vladimir Lifschitz (1998) "Action Languages", <i>Linköping Electronic Articles in Computer and Information Science</i>, vol. <b>3</b>, nr. <i>16</i>.</span>

</li>

</ol></div></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox authority-control" aria-label="Navbox390" style="padding:3px"><table class="nowraplinks hlist navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Authority control databases: National </th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://d-nb.info/gnd/4329099-1">Germany</a></span></li></ul></div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-11-03" href="https://en.wikipedia.org/wiki/?title=Transition_system&oldid=1255090777">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>